package org.lemma.language.sequent;

import java.util.ArrayList;
import java.util.Iterator;
import javax.annotation.Author;
import javax.annotation.Copyright;
import javax.annotation.Version;
import org.lemma.language.Operator;
import org.lemma.language.Formula;
import org.lemma.set.FiniteHashSet;
import org.lemma.set.FiniteSet;

/**
 * <p>
 *  TODO: Javadoc for {@code Sequent}
 * </p>
 *
 * @author Chris Beatty [christopher.beatty@gmail.com]
 * @version 1.0.0
 */
@Version (
    major="1", minor="0", patch="0", 
    date="Sep 3, 2008 9:47:12 AM",
    authors = {
        @Author (name="Chris Beatty", email="christopher.beatty@gmail.com")
    }
) @Copyright 
public class Sequent extends Operator {

   /**
     * Determines if a de-serialized file is compatible with this class.
     *
     * Maintainers must change this value if and only if the new version
     * of this class is not compatible with old versions. See Sun docs
     * for <a href="http://java.sun.com/products/jdk/1.1/docs/guide
     * /serialization/spec/version.doc.html">details.</a>
     */
    private static final long serialVersionUID = 1L;

    /**
     *
     */
    private FiniteSet<Formula> resolvents = null;

    /**
     *
     */
    protected Sequent() {
        super();
    }

    /**
     *
     * @param operator
     * @param antecedent
     * @param succedent
     */
    public Sequent(String operator, FiniteSet<Formula> antecedent, FiniteSet<Formula> succedent) {
        super(operator, new ArrayList<Formula>(antecedent));
        this.resolvents = succedent;
    }

    /**
     * {@inheritDoc}
     *
     * @param obj {@inheritDoc}
     * @return {@inheritDoc}
     */
    @Override
    public boolean equals(Object obj) {
        if (obj == null) {
            return false;
        }
        if (getClass() != obj.getClass()) {
            return false;
        }
        final Sequent other = (Sequent) obj;
        if (!super.equals(other)) {
            return false;
        }
        if (this.resolvents != other.resolvents && (this.resolvents == null || !this.resolvents.equals(other.resolvents))) {
            return false;
        }
        return true;
    }

    /**
     * {@inheritDoc}
     *
     * @return {@inheritDoc}
     */
    @Override
    public int hashCode() {
        int hash = super.hashCode();
        hash = 53 * hash + (this.resolvents != null ? this.resolvents.hashCode() : 0);
        return hash;
    }

    /**
     * {@inheritDoc}
     *
     * @return {@inheritDoc}
     */
    @Override
    public Sequent clone() {
        //Copy operands
        FiniteSet<Formula> ops = new FiniteHashSet<Formula>();
        for(Formula formula : this.operands()) {
            ops.add(formula.clone());
        }
        //Copy resolvents
        FiniteSet<Formula> res = new FiniteHashSet<Formula>();
        for(Formula formula : this.resolvents) {
            res.add(formula.clone());
        }
        return new Sequent(new String(this.symbol()), ops, res);
    }

    /**
     * {@inheritDoc}
     * 
     * @return {@inheritDoc}
     */
    @Override
    public String toString() {
        StringBuilder sb = new StringBuilder();
        for(Iterator i = this.operands().iterator(); i.hasNext(); ) {
            sb.append(i.next());
            if(i.hasNext()) {
                sb.append(", ");
            } else {
                sb.append(" ");
            }
        }
        sb.append(this.symbol());
        for(Iterator i = this.resolvents.iterator(); i.hasNext(); ) {
            sb.append(i.next());
            if(i.hasNext()) {
                sb.append(", ");
            }
        }
        return sb.toString();
    }

}
